A, B, C:Type, as:(A List), bs:(B List), F:(ABC).
cs:C List. (c:C. (c  cs)  (aas.(bbs.c = F(a,b)))) 

latex

Definitions	{T}, P  Q, P & Q, P  Q, P  Q, x. t(x), , P  Q, x:A. B(x), t  T, x:A. B(x), False, x(s), (xL.P(x))
Lemmas	l exists cons, member map, or functionality wrt iff, member append, map wf, append wf, nil member, l exists nil, iff functionality wrt iff, all functionality wrt iff, false wf, l exists wf, l member wf, iff wf